Skip to content

[Relay] Check match expressions for completeness - #3203

Merged
tqchen merged 8 commits into
apache:masterfrom
slyubomirsky:match-exhaustion
Jun 13, 2019
Merged

[Relay] Check match expressions for completeness#3203
tqchen merged 8 commits into
apache:masterfrom
slyubomirsky:match-exhaustion

Conversation

@slyubomirsky

@slyubomirsky slyubomirsky commented May 16, 2019

Copy link
Copy Markdown
Contributor

We never defined the semantics of an incomplete match in Relay, so I've written a fairly simple function to check whether a match is complete (there's probably a better algorithm, but this one also concretely finds all cases that are not handled) and added into the type checker.

This did require me to change several functions that relied on having incomplete matches, such as hd and tl. I do not think we should permit partial functions, as that would require us to define semantics for incomplete matches and potentially, down the line, to complicate the language with other kinds of error handling that could be placed higher in the stack (e.g., it would be a problem if some execution settings for Relay had one kind of error for incomplete matches and others reported the error a different way).

I suppose, though, that it would be easy to change the match incompleteness to a warning rather than an error if we really do want to keep hd, tl, etc.

Incomplete matches only generate a warning for now, though we may want to add flags to make this an error later, see @MarisaKirisame's comment below

@MarisaKirisame

Copy link
Copy Markdown
Contributor

@slyubomirsky can you make it LOG(WARNING) if a pattern is not exhausted right now? I think we should touch the hd/nth/tl function later.
So I think there is 3 pr:
0: the exhaustiveness checker that warn stuff
1: a flag 'strict' in the match node that check for exhaustiveness, and possibly redundancy later
2: discuss what to do with the partial functions, as @icemelon9 is using them.
I think we can take a similar approach as http://hackage.haskell.org/package/safe: provide version that is easiest to use, provide one that return default, provide one that return Maybe, etc.

@slyubomirsky

Copy link
Copy Markdown
Contributor Author

I agree, I'll make it a warning

@MarisaKirisame

Copy link
Copy Markdown
Contributor

@slyubomirsky http://moscova.inria.fr/~maranget/papers/warn/index.html
this paper conver redundancy as well. It's exhaustiveness algorithm is different. I think we can keep ours as it is, unless it get too slow.

@tqchen

tqchen commented May 24, 2019

Copy link
Copy Markdown
Member

Comment thread src/relay/pass/match_exhaustion.cc Outdated
for (size_t i = 0; i < op->patterns.size(); i++) {
MatchResult submatch = this->Check(op->patterns[i], ctor_cand->patterns[i]);
if (submatch != MatchResult::kMatch) {
return submatch;

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

you can be more aggressive here: if any of the child is clash, return clash

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point, I'll do that.

@MarisaKirisame

Copy link
Copy Markdown
Contributor

one small nitpick, otherwise is good.

@slyubomirsky

Copy link
Copy Markdown
Contributor Author

Pinging @MarisaKirisame and @icemelon9 for final review

@tqchen
tqchen merged commit a698ad7 into apache:master Jun 13, 2019
wweic pushed a commit to wweic/tvm that referenced this pull request Jun 26, 2019
wweic pushed a commit to neo-ai/tvm that referenced this pull request Jun 27, 2019
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants